E7: -fverify-* options for clang++ builds, a report per object, and quiet files without contracts - #120

Plan item E7 (verification inside clang++ builds): a compilation verified every file with the defaults (Z3, 30 s a query, one job) whatever it needed, and every file without contracts warned, so a build that gave -fverify-contracts to every file printed a warning for most of them.

On the base

$ clang++ -std=c++17 -fverify-contracts -c plain.cpp -o plain.o      # int add(int a, int b) { return a + b; }
warning: no verifiable functions found [-Wcppverify]
1 warning generated.
$ clang++ -std=c++17 -fverify-contracts -fverify-timeout=5000 -c ok.cpp -o ok.o
clang++: error: unknown argument: '-fverify-timeout=5000'

With this PR

$ clang++ -std=c++17 -fverify-contracts -Rcppverify -fverify-report -c ok.cpp -o ok.o
ok.cpp:2:5: remark: Verified: inc [backend=z3] [-Rcppverify]
$ cat ok.o.cppverify.json
{"backend":"z3","function":"inc","function_source":{...},"message":"inc [backend=z3]","schema":"cppverify.diagnostic/2","severity":"note","status":"verified"}
{"bounded_safe":0,"exported":0,"failed":0,"interrupted":0,"lowered":0,"reasons":{},"schema":"cppverify.summary/1","trusted":0,"unresolved":0,"verified":1}
$ clang++ -std=c++17 -fverify-contracts -c plain.cpp -o plain.o
$ clang++ -std=c++17 -fverify-contracts -fverify-backend=lean -c ok.cpp -o ok.o
error: invalid value 'lean' in '-fverify-backend=lean'

A file without a function to verify says nothing (cpp-verify still warns for one: a run asked to verify it).

Design

• Clang's own options. The options are FrontendOptions fields parsed by Clang's option marshalling (MarshallingInfoEnum for the backend, MarshallingInfoInt for the numbers), so an invalid value is the compiler's usual error, and the driver forwards them as it forwards -fverify-contracts-out=.
• A report per object, as -ftime-trace does. In a build the same flag goes to every file, so a bare -fverify-report writes <object>.cppverify.json beside each object: the driver, which knows the output, passes -fverify-report=<path> to the compiler, as -ftime-trace names its file after the object. The report is the records cpp-verify --diagnostics-format=json prints, then the summary record; the summary record is built in one place now (summaryRecord), which cpp-verify uses too.
• The tool's meaning for the tool's names. compilationOptions maps the options as cpp-verify maps --timeout, --jobs, --backend, and --proof-cache, including the timeouts a query timeout scales. The proof cache already writes atomically and prunes once per run, so compilations may share a directory.
• Quiet on success. A proof is a remark (E3); with QuietWithoutFunctions a file without contracts is no longer a warning.
• The upstream hook stays one line: CodeGenAction passes the FrontendOptions instead of one field.

Tests

• compile_options.cpp (new): the driver forwards every option and names a bare -fverify-report's file after the object, or keeps the file given; an invalid backend or timeout is the compiler's error; a file without contracts compiles with no output at all (count 0); -fverify-backend=bmc reaches the verifier ([backend=bmc, bound=0]), with a proof and a failure, and -fverify-report= holds both records and a summary of one verified and one failed; -fverify-cache= fills the directory.
• CompilationOptionsTest (new, VerifyTests): the defaults, which must equal cpp-verify's own, each option, every backend, -fverify-timeout=0 disabling every limit as --timeout=0 does, and the extremes (0 jobs is 1; a timeout too large to scale gives no collection and function bounds, as cpp-verify).

On the base compile_options.cpp fails at its first option (unknown argument), and the file without contracts warns.

On a release build of this branch, the whole Verify suite passes (505 of 506, one unsupported) once a stale BUG_REPORT_URL in the local CMake cache is cleared; with it crash_report_url.cpp names LLVM's tracker, which a fresh configure, as CI's, does not.

Mutants

Each mutant below, applied alone and rebuilt, is caught (10 of 10):

Review also found that -fverify-timeout=0 first meant the default, where cpp-verify --timeout=0 disables the limit; the option now defaults to 30000 and 0 disables, as for the tool.

Docs

• Tooling: "Options of a compilation" (the table, the errors, the quiet file) and "Verification in a CMake build", a recipe with -fno-verify for development builds;
• the toolchain chapter: "Verification in a build";
• release notes; ARCHITECTURE (Compile-Time Integration).

Not done

• -fverify-* options for the Lean backend, and for --function or --max-failures: a compilation verifies the whole file with a solver.
• A cache of whole functions' results (C8): the cache keeps proofs of single obligations, so an unchanged file is not free, only cheaper.